Runtime Complexity (innermost) proof of /tmp/tmpmZhGQH/sat.xml

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).

0 CpxTRS

↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 13 ms)

↳2 CdtProblem

↳3 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)

↳4 CdtProblem

↳5 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID), 0 ms)

↳6 CdtProblem

↳7 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

↳8 CdtProblem

↳9 CdtLeafRemovalProof (ComplexityIfPolyImplication, 0 ms)

↳10 CdtProblem

↳11 CdtKnowledgeProof (BOTH BOUNDS(ID, ID), 0 ms)

↳12 CdtProblem

↳13 CdtUsableRulesProof (⇔, 0 ms)

↳14 CdtProblem

↳15 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 158 ms)

↳16 CdtProblem

↳17 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 33 ms)

↳18 CdtProblem

↳19 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 78 ms)

↳20 CdtProblem

↳21 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 49 ms)

↳22 CdtProblem

↳23 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 15 ms)

↳24 CdtProblem

↳25 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)

↳26 BOUNDS(1, 1)

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^2).

The TRS R consists of the following rules:

if(true, t, e) → t
if(false, t, e) → e
member(x, nil) → false
member(x, cons(y, ys)) → if(eq(x, y), true, member(x, ys))
eq(nil, nil) → true
eq(O(x), 0(y)) → eq(x, y)
eq(0(x), 1(y)) → false
eq(1(x), 0(y)) → false
eq(1(x), 1(y)) → eq(x, y)
negate(0(x)) → 1(x)
negate(1(x)) → 0(x)
choice(cons(x, xs)) → x
choice(cons(x, xs)) → choice(xs)
guess(nil) → nil
guess(cons(clause, cnf)) → cons(choice(clause), guess(cnf))
verify(nil) → true
verify(cons(l, ls)) → if(member(negate(l), ls), false, verify(ls))
sat(cnf) → satck(cnf, guess(cnf))
satck(cnf, assign) → if(verify(assign), assign, unsat)

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted Cpx (relative) TRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
eq(nil, nil) → true
eq(O(z0), 0(z1)) → eq(z0, z1)
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
sat(z0) → satck(z0, guess(z0))
satck(z0, z1) → if(verify(z1), z1, unsat)

Tuples:

IF(true, z0, z1) → c
IF(false, z0, z1) → c1
MEMBER(z0, nil) → c2
MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(nil, nil) → c4
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(0(z0), 1(z1)) → c6
EQ(1(z0), 0(z1)) → c7
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
NEGATE(0(z0)) → c9
NEGATE(1(z0)) → c10
CHOICE(cons(z0, z1)) → c11
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(nil) → c13
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(nil) → c15
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))

S tuples:

IF(true, z0, z1) → c
IF(false, z0, z1) → c1
MEMBER(z0, nil) → c2
MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(nil, nil) → c4
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(0(z0), 1(z1)) → c6
EQ(1(z0), 0(z1)) → c7
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
NEGATE(0(z0)) → c9
NEGATE(1(z0)) → c10
CHOICE(cons(z0, z1)) → c11
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(nil) → c13
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(nil) → c15
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))

K tuples:none
Defined Rule Symbols:

if, member, eq, negate, choice, guess, verify, sat, satck

Defined Pair Symbols:

IF, MEMBER, EQ, NEGATE, CHOICE, GUESS, VERIFY, SAT, SATCK

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 11 trailing nodes:

GUESS(nil) → c13
EQ(0(z0), 1(z1)) → c6
VERIFY(nil) → c15
CHOICE(cons(z0, z1)) → c11
NEGATE(0(z0)) → c9
EQ(1(z0), 0(z1)) → c7
IF(false, z0, z1) → c1
IF(true, z0, z1) → c
EQ(nil, nil) → c4
MEMBER(z0, nil) → c2
NEGATE(1(z0)) → c10

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
eq(nil, nil) → true
eq(O(z0), 0(z1)) → eq(z0, z1)
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
sat(z0) → satck(z0, guess(z0))
satck(z0, z1) → if(verify(z1), z1, unsat)

Tuples:

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))

S tuples:

MEMBER(z0, cons(z1, z2)) → c3(IF(eq(z0, z1), true, member(z0, z2)), EQ(z0, z1), MEMBER(z0, z2))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(IF(member(negate(z0), z1), false, verify(z1)), MEMBER(negate(z0), z1), NEGATE(z0), VERIFY(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
SATCK(z0, z1) → c18(IF(verify(z1), z1, unsat), VERIFY(z1))

K tuples:none
Defined Rule Symbols:

if, member, eq, negate, choice, guess, verify, sat, satck

Defined Pair Symbols:

MEMBER, EQ, CHOICE, GUESS, VERIFY, SAT, SATCK

Compound Symbols:

c3, c5, c8, c12, c14, c16, c17, c18

(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 4 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
eq(nil, nil) → true
eq(O(z0), 0(z1)) → eq(z0, z1)
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
sat(z0) → satck(z0, guess(z0))
satck(z0, z1) → if(verify(z1), z1, unsat)

Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))

S tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
SAT(z0) → c17(SATCK(z0, guess(z0)), GUESS(z0))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))

K tuples:none
Defined Rule Symbols:

if, member, eq, negate, choice, guess, verify, sat, satck

Defined Pair Symbols:

EQ, CHOICE, GUESS, SAT, MEMBER, VERIFY, SATCK

Compound Symbols:

c5, c8, c12, c14, c17, c3, c16, c18

(7) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
eq(nil, nil) → true
eq(O(z0), 0(z1)) → eq(z0, z1)
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
sat(z0) → satck(z0, guess(z0))
satck(z0, z1) → if(verify(z1), z1, unsat)

Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))
SAT(z0) → c(GUESS(z0))

S tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))
SAT(z0) → c(GUESS(z0))

K tuples:none
Defined Rule Symbols:

if, member, eq, negate, choice, guess, verify, sat, satck

Defined Pair Symbols:

EQ, CHOICE, GUESS, MEMBER, VERIFY, SATCK, SAT

Compound Symbols:

c5, c8, c12, c14, c3, c16, c18, c

(9) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

Removed 1 leading nodes:

SAT(z0) → c(GUESS(z0))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
eq(nil, nil) → true
eq(O(z0), 0(z1)) → eq(z0, z1)
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
sat(z0) → satck(z0, guess(z0))
satck(z0, z1) → if(verify(z1), z1, unsat)

Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))

S tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))

K tuples:none
Defined Rule Symbols:

if, member, eq, negate, choice, guess, verify, sat, satck

Defined Pair Symbols:

EQ, CHOICE, GUESS, MEMBER, VERIFY, SATCK, SAT

Compound Symbols:

c5, c8, c12, c14, c3, c16, c18, c

(11) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

The following tuples could be moved from S to K by knowledge propagation:

SAT(z0) → c(SATCK(z0, guess(z0)))
SATCK(z0, z1) → c18(VERIFY(z1))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
eq(nil, nil) → true
eq(O(z0), 0(z1)) → eq(z0, z1)
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
sat(z0) → satck(z0, guess(z0))
satck(z0, z1) → if(verify(z1), z1, unsat)

Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))

S tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))

K tuples:

SAT(z0) → c(SATCK(z0, guess(z0)))
SATCK(z0, z1) → c18(VERIFY(z1))

Defined Rule Symbols:

if, member, eq, negate, choice, guess, verify, sat, satck

Defined Pair Symbols:

EQ, CHOICE, GUESS, MEMBER, VERIFY, SATCK, SAT

Compound Symbols:

c5, c8, c12, c14, c3, c16, c18, c

(13) CdtUsableRulesProof (EQUIVALENT transformation)

The following rules are not usable and were removed:

if(true, z0, z1) → z0
if(false, z0, z1) → z1
member(z0, nil) → false
member(z0, cons(z1, z2)) → if(eq(z0, z1), true, member(z0, z2))
eq(nil, nil) → true
eq(O(z0), 0(z1)) → eq(z0, z1)
eq(0(z0), 1(z1)) → false
eq(1(z0), 0(z1)) → false
eq(1(z0), 1(z1)) → eq(z0, z1)
verify(nil) → true
verify(cons(z0, z1)) → if(member(negate(z0), z1), false, verify(z1))
sat(z0) → satck(z0, guess(z0))
satck(z0, z1) → if(verify(z1), z1, unsat)

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)

Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))

S tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))

K tuples:

SAT(z0) → c(SATCK(z0, guess(z0)))
SATCK(z0, z1) → c18(VERIFY(z1))

Defined Rule Symbols:

negate, guess, choice

Defined Pair Symbols:

EQ, CHOICE, GUESS, MEMBER, VERIFY, SATCK, SAT

Compound Symbols:

c5, c8, c12, c14, c3, c16, c18, c

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))

We considered the (Usable) Rules:none
And the Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = 0
POL(1(x₁)) = 0
POL(CHOICE(x₁)) = x₁
POL(EQ(x₁, x₂)) = 0
POL(GUESS(x₁)) = [2]x₁
POL(MEMBER(x₁, x₂)) = 0
POL(O(x₁)) = 0
POL(SAT(x₁)) = [2] + [2]x₁
POL(SATCK(x₁, x₂)) = [1] + x₁
POL(VERIFY(x₁)) = 0
POL(c(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c18(x₁)) = x₁
POL(c3(x₁, x₂)) = x₁ + x₂
POL(c5(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(choice(x₁)) = 0
POL(cons(x₁, x₂)) = [2] + x₁ + x₂
POL(guess(x₁)) = 0
POL(negate(x₁)) = 0
POL(nil) = 0

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)

Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))

S tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))

K tuples:

SAT(z0) → c(SATCK(z0, guess(z0)))
SATCK(z0, z1) → c18(VERIFY(z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))

Defined Rule Symbols:

negate, guess, choice

Defined Pair Symbols:

EQ, CHOICE, GUESS, MEMBER, VERIFY, SATCK, SAT

Compound Symbols:

c5, c8, c12, c14, c3, c16, c18, c

(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))

We considered the (Usable) Rules:

guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))

And the Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = 0
POL(1(x₁)) = 0
POL(CHOICE(x₁)) = 0
POL(EQ(x₁, x₂)) = 0
POL(GUESS(x₁)) = 0
POL(MEMBER(x₁, x₂)) = 0
POL(O(x₁)) = 0
POL(SAT(x₁)) = [1] + x₁
POL(SATCK(x₁, x₂)) = [1] + x₂
POL(VERIFY(x₁)) = x₁
POL(c(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c18(x₁)) = x₁
POL(c3(x₁, x₂)) = x₁ + x₂
POL(c5(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(choice(x₁)) = 0
POL(cons(x₁, x₂)) = [1] + x₂
POL(guess(x₁)) = x₁
POL(negate(x₁)) = 0
POL(nil) = 0

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)

Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))

S tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))

K tuples:

SAT(z0) → c(SATCK(z0, guess(z0)))
SATCK(z0, z1) → c18(VERIFY(z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))

Defined Rule Symbols:

negate, guess, choice

Defined Pair Symbols:

EQ, CHOICE, GUESS, MEMBER, VERIFY, SATCK, SAT

Compound Symbols:

c5, c8, c12, c14, c3, c16, c18, c

(19) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))

We considered the (Usable) Rules:

negate(1(z0)) → 0(z0)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
negate(0(z0)) → 1(z0)

And the Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = [1]
POL(1(x₁)) = 0
POL(CHOICE(x₁)) = 0
POL(EQ(x₁, x₂)) = [1]
POL(GUESS(x₁)) = 0
POL(MEMBER(x₁, x₂)) = [2] + [2]x₁ + x₂ + [2]x₁·x₂
POL(O(x₁)) = [2]
POL(SAT(x₁)) = [1] + [2]x₁ + x₁²
POL(SATCK(x₁, x₂)) = [2]x₂ + x₂²
POL(VERIFY(x₁)) = [2]x₁ + x₁²
POL(c(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c18(x₁)) = x₁
POL(c3(x₁, x₂)) = x₁ + x₂
POL(c5(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(choice(x₁)) = [1] + x₁ + x₁²
POL(cons(x₁, x₂)) = [2] + x₂
POL(guess(x₁)) = x₁
POL(negate(x₁)) = [1]
POL(nil) = 0

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)

Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))

S tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))

K tuples:

SAT(z0) → c(SATCK(z0, guess(z0)))
SATCK(z0, z1) → c18(VERIFY(z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))

Defined Rule Symbols:

negate, guess, choice

Defined Pair Symbols:

EQ, CHOICE, GUESS, MEMBER, VERIFY, SATCK, SAT

Compound Symbols:

c5, c8, c12, c14, c3, c16, c18, c

(21) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))

We considered the (Usable) Rules:

negate(1(z0)) → 0(z0)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
choice(cons(z0, z1)) → choice(z1)
choice(cons(z0, z1)) → z0
negate(0(z0)) → 1(z0)

And the Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = x₁
POL(1(x₁)) = x₁
POL(CHOICE(x₁)) = 0
POL(EQ(x₁, x₂)) = [2]x₁
POL(GUESS(x₁)) = 0
POL(MEMBER(x₁, x₂)) = [2]x₁ + [2]x₁·x₂
POL(O(x₁)) = [2] + x₁
POL(SAT(x₁)) = [2] + x₁ + x₁²
POL(SATCK(x₁, x₂)) = [2] + x₁ + x₂²
POL(VERIFY(x₁)) = [1] + x₁²
POL(c(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c18(x₁)) = x₁
POL(c3(x₁, x₂)) = x₁ + x₂
POL(c5(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(choice(x₁)) = x₁
POL(cons(x₁, x₂)) = [2] + x₁ + x₂
POL(guess(x₁)) = x₁
POL(negate(x₁)) = [2] + x₁
POL(nil) = 0

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)

Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))

S tuples:

EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))

K tuples:

SAT(z0) → c(SATCK(z0, guess(z0)))
SATCK(z0, z1) → c18(VERIFY(z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))

Defined Rule Symbols:

negate, guess, choice

Defined Pair Symbols:

EQ, CHOICE, GUESS, MEMBER, VERIFY, SATCK, SAT

Compound Symbols:

c5, c8, c12, c14, c3, c16, c18, c

(23) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))

We considered the (Usable) Rules:

negate(1(z0)) → 0(z0)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
choice(cons(z0, z1)) → choice(z1)
choice(cons(z0, z1)) → z0
negate(0(z0)) → 1(z0)

And the Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(0(x₁)) = [2] + x₁
POL(1(x₁)) = [1] + x₁
POL(CHOICE(x₁)) = 0
POL(EQ(x₁, x₂)) = x₁·x₂
POL(GUESS(x₁)) = [2]x₁
POL(MEMBER(x₁, x₂)) = [2]x₁·x₂
POL(O(x₁)) = [2] + x₁
POL(SAT(x₁)) = [1] + [2]x₁ + [2]x₁²
POL(SATCK(x₁, x₂)) = [1] + x₁ + [2]x₂²
POL(VERIFY(x₁)) = [2]x₁²
POL(c(x₁)) = x₁
POL(c12(x₁)) = x₁
POL(c14(x₁, x₂)) = x₁ + x₂
POL(c16(x₁, x₂)) = x₁ + x₂
POL(c18(x₁)) = x₁
POL(c3(x₁, x₂)) = x₁ + x₂
POL(c5(x₁)) = x₁
POL(c8(x₁)) = x₁
POL(choice(x₁)) = x₁
POL(cons(x₁, x₂)) = x₁ + x₂
POL(guess(x₁)) = x₁
POL(negate(x₁)) = [2]x₁
POL(nil) = 0

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

negate(0(z0)) → 1(z0)
negate(1(z0)) → 0(z0)
guess(nil) → nil
guess(cons(z0, z1)) → cons(choice(z0), guess(z1))
choice(cons(z0, z1)) → z0
choice(cons(z0, z1)) → choice(z1)

Tuples:

EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
SATCK(z0, z1) → c18(VERIFY(z1))
SAT(z0) → c(SATCK(z0, guess(z0)))

S tuples:none
K tuples:

SAT(z0) → c(SATCK(z0, guess(z0)))
SATCK(z0, z1) → c18(VERIFY(z1))
CHOICE(cons(z0, z1)) → c12(CHOICE(z1))
GUESS(cons(z0, z1)) → c14(CHOICE(z0), GUESS(z1))
VERIFY(cons(z0, z1)) → c16(MEMBER(negate(z0), z1), VERIFY(z1))
MEMBER(z0, cons(z1, z2)) → c3(EQ(z0, z1), MEMBER(z0, z2))
EQ(O(z0), 0(z1)) → c5(EQ(z0, z1))
EQ(1(z0), 1(z1)) → c8(EQ(z0, z1))

Defined Rule Symbols:

negate, guess, choice

Defined Pair Symbols:

EQ, CHOICE, GUESS, MEMBER, VERIFY, SATCK, SAT

Compound Symbols:

c5, c8, c12, c14, c3, c16, c18, c

(25) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty

(0) Obligation:

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

(2) Obligation:

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

(4) Obligation:

(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

(6) Obligation:

(7) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

(8) Obligation:

(9) CdtLeafRemovalProof (ComplexityIfPolyImplication transformation)

(10) Obligation:

(11) CdtKnowledgeProof (BOTH BOUNDS(ID, ID) transformation)

(12) Obligation:

(13) CdtUsableRulesProof (EQUIVALENT transformation)

(14) Obligation:

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(16) Obligation:

(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)

(18) Obligation:

(19) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

(20) Obligation:

(21) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

(22) Obligation:

(23) CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)) transformation)

(24) Obligation:

(25) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

(26) BOUNDS(1, 1)